(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(b(b(x1))) → P(a(b(x1)))
a(P(x1)) → P(a(x(x1)))
a(x(x1)) → x(a(x1))
b(P(x1)) → b(Q(x1))
Q(x(x1)) → a(Q(x1))
Q(a(x1)) → b(b(a(x1)))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.
Start state: 1277
Accept states: [1278, 1279, 1280]
Transitions:
1277→1278[a_1|0]
1277→1279[b_1|0]
1277→1280[Q_1|0]
1277→1277[P_1|0, x_1|0]
1277→1281[x_1|1]
1277→1283[Q_1|1]
1277→1284[a_1|1]
1277→1285[Q_1|1]
1277→1286[a_1|2]
1281→1282[a_1|1]
1282→1278[P_1|1]
1282→1284[P_1|1]
1282→1286[P_1|1]
1283→1279[b_1|1]
1284→1278[x_1|1]
1284→1284[x_1|1]
1284→1286[x_1|1]
1285→1280[a_1|1]
1285→1283[a_1|1]
1285→1285[a_1|1]
1286→1282[x_1|2]

(2) BOUNDS(O(1), O(n^1))